﻿/************************************************************************
 * SMLib - State Model Library
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     SMLib\Storage\CTMC.cs
 * Description  :     Implementation of BDD Structure: Used in model checking engine - MCGine
 *                    (c) Ali Khalili and Amir Jalaly
 * Change log   :     -Jan 2012: some mofifications
 *                    -2011:  Initial version
 * To Do        :     1-Use this instead of previous class and structures (DONE!)
 *                    2-Remove the second algorithm for state space generation
 *                    3-On the fly computation of rewards
 ************************************************************************/
using System;
using System.Collections.Generic;
using System.Reflection;
using SMLib.Utils;
using SMLib.Base;

namespace SMLib.Storage
{
	/// <summary>
	///  It is using an explicit state representation for the states in the state space
	/// </summary>
	public class CTMC_StateSpace : 
        DiGraph<CTMCState,CTMCState.Transition>,
        ISqMatrix<double>
	{


		//[To Do]Not efficient. Compute rewards on the fly!
		public SortedList<string, double> Rewards = new SortedList<string, double> ();
		
		public bool exportProbabilities = false;

		/// <summary>
		/// Check to make sure that it is not reduceable!
		/// </summary>
		/// <returns></returns>
		public bool Check ()
		{
			throw new Exception ("Not implemented yet!");
		}


        #region Second algorithm to reduce vanishing states
		///<summary>
		///Reduce a currentState space set with zero-rate actions (immediate) to a CTMC
		///</summary>
		public void ReduceToCTMC ()
		{
            #region remove transitions with the same destinationContent
			for (int i = 0; i < states.Count; i++) {
				CTMCState state = (CTMCState)states [i];
				for (int j = state.Transitions.Count - 1; j >= 0; j--) {
					for (int k = state.Transitions.Count - 1; k >= 0; k--) {
						CTMCState.Transition t1 = (CTMCState.Transition)state.Transitions [j];
						CTMCState.Transition t2 = (CTMCState.Transition)state.Transitions [k];
						if (t1.Destination == t2.Destination && k != j) {
							if (t1.Rate * t2.Rate > 0)
								t1.Rate += t2.Rate;
							else
								t1.Rate = Math.Min (t1.Rate, t2.Rate);
							t2.Rate = 0;
							state.Transitions.RemoveAt (k);
						}
					}
				}
				//for (int j = currentState.transitions.Count - 1; j >= 0; j--)
				//{
				//    State.Transition t1 = currentState.transitions[j];
				//    if (t1.rate == 0) currentState.transitions.RemoveAt(j);
				//}
			}

            #endregion

			for (int i = states.Count - 1; i >= 0; i--) {
				i = Math.Min (i, states.Count - 1);
				CTMCState state = (CTMCState)states [i];
				while (ReduceState(state))
					;
			}


			//[To Do]Make it working and then remove it!!!!
			//if (initialstate.Count > 0)
			//{
			//    InitialState state = initialstate[0];
			//    if (HasInstanteneos(state.state))
			//    {
			//        double sum = 0;
			//        foreach (CTMCState.Transition t in state.state.transitions)
			//        {
			//            if (t.rate < 0)
			//                sum += t.rate;
			//        }
			//        initialstate.Remove(state);
			//        states.Remove((CTMCState)state.state);
			//        foreach (State.Transition t in state.state.transitions)
			//        {
			//            //t.Destination = null;
			//            if (t.rate < 0)
			//                initialstate.Add(new InitialState((State)t.Destination, t.rate / sum));
			//        }

			//    }
			//}
		}

		/// <summary>
		/// This is used by State space reduction algorithm (here)
		/// </summary>
		/// <param name="source"></param>
		/// <param name="destinationContent"></param>
		/// <param name="rate"></param>
		//[To Do:Remove]
		protected void AddTransition (CTMCState source, CTMCState destination, double rate)
		{
			foreach (CTMCState.Transition t in source.Transitions) {
				if (t.Destination == destination) {
					t.Rate += rate;
					return;
				}
			}
			source.Transitions.Add (new CTMCState.Transition (rate, destination));
		}


		///<summary>
		///Reduce one currentState (remove transitions with  rate infinity, i.e. immediate transitions)
		///</summary>
		/// <param name="path">The currentState that is going to be reduced</param>
		bool ReduceState (CTMCState state)
		{
			bool checkagain = false;
			for (int i = state.Transitions.Count - 1; i >= 0; i--) {
				CTMCState.Transition tran = (CTMCState.Transition)state.Transitions [i];
				//if (tran.rate < 0)
				//    continue;
				if (HasInstanteneos ((CTMCState)tran.Destination)) {
					checkagain = true;
					states.Remove ((CTMCState)tran.Destination);
					double sum = 0;
					foreach (CTMCState.Transition t in ((CTMCState)tran.Destination).Transitions) {
						if (t.Rate < 0)
							sum += t.Rate;
					}
					foreach (CTMCState.Transition t in ((CTMCState)tran.Destination).Transitions) {
						if (t.Rate < 0)
                            //currentState.addTransition((State)t.Destination, tran.rate * t.rate / sum);
							AddTransition (state, (CTMCState)t.Destination, tran.Rate * t.Rate / sum);
					}
					state.Transitions.Remove (tran);

				}
			}
			return checkagain;
		}


		///<summary>
		///Check thet is an currentState is reduceable or not (has any immediate outgoing transition or not)
		///</summary>
		/// <param name="path">The currentState that is going to be checked</param>
		private bool HasInstanteneos (CTMCState stateSpace)
		{
			foreach (CTMCState.Transition t in stateSpace.Transitions) {
				if (t.Rate < 0)
					return true;
			}
			return false;
		}


        #endregion


		/// <summary>
		/// .[To Do]This is used for simple solving. I will remove this method or improve it
		/// </summary>
		/// <param name="a"></param>
		public void ConverToMatrix (Matrix a)
		{
			double sum = 0;
			for (int i = 0; i < states.Count; i++) {
				for (int j = 0; j < states[i].Transitions.Count; j++) {
					a.setValue (
                        ((CTMCState)((CTMCState.Transition)states [i].Transitions [j]).Destination).id - 1,
                            i, ((CTMCState.Transition)states [i].Transitions [j]).Rate);
				}
			}
			for (int i = 0; i < states.Count; i++) {
				sum = 0;
				for (int j = 0; j < states.Count; j++) {
					sum += a.getValue (j, i);
				}
				a.setValue (i, i, -sum);
			}
		}

        #region ICTMCMatrix Members

		///// <summary>
		///// Numbe of states in the CTMC
		///// </summary>
		//public int Count
		//{
		//    get
		//    {
		//        return states.Count;
		//    }
		//}

		/// <summary>
		/// Return the the rate in CTMC Matrix in the Column 'i' and Row 'j'
		/// Note: Before using this method, call ReduceToCTMC (to convert statse space to CTMC)
		/// Warning: parameters should be less than the size of currentState sace
		/// </summary>
		/// <param name="i">Row number</param>
		/// <param name="j">Column number </param>
		/// <returns></returns>
		public double CTMCRate (int i, int j)
		{
			CTMCState ss = (CTMCState)states [i];
			//We suppose that i and j are in boundry
			//if (i > this.Count || i < 0 || j < 0 || j > this.Count)
			//    throw new exception();

			if (i == this.Size - 1) {
				//All element in the last row are zero
				return 1;
			} else if (i != j) {
				//Transition to other states
				foreach (CTMCState.Transition t in ss.Transitions)
					if (t.Destination == this [j] && t.Destination != ss) // We eliminate transition to itself!
						return t.Rate;
			} else if (i == j) {
				//Transition to itself
				double sumAllRates = 0;
				foreach (CTMCState.Transition t in ss.Transitions)
                    //Change Log (23 sep 2011): We eliminate transition to itself!
					if (t.Destination != ss)
						sumAllRates += t.Rate;

				return -1 * sumAllRates;
			}
			return 0;
		}

        #endregion


		/// <summary>
		/// Return the rate value from the one currentState to another currentState (in the raw currentState space set)
		/// </summary>
		/// <param name="i">Source currentState</param>
		/// <param name="j">Destination currentState</param>
		/// <returns>transition rate</returns>
		public double this [int i, int j] {
			get {
				CTMCState ss = (CTMCState)states [i];
				//* Transition to other states
				foreach (CTMCState.Transition t in ss.Transitions)
					if (t.Destination == this [j])
						return t.Rate;
				return 0;
			}
			set {
				throw new Exception ("Not implemented yet");
			}
		}


		//#region Re-Write abstract methods
		//protected override IStateContainer newStateContainer(/*IStateContent*/object content)
		//{
		//    return new CTMCState(states.Count, content);
		//}

		//protected override ITransition newTransition(IStateContainer st, object tr)
		//{
		//    return new CTMCState.Transition((double)tr, (CTMCState)st);
		//}

		//protected override void UpdateTransition(IStateContainer src, ITransition tr, object newTr)
		//{
		//    ((CTMCState.Transition)tr).Rate += (double)newTr;
		//}

		///////<summary>
		///////Save the currentState space into a specified file 
		///////</summary>
		/////// <param name="path">Used to indicate the path.</param>
		////public override void ExportAsXML(string path)
		////{
		////    XmlDatabaseHelper db = new XmlDatabaseHelper();

		////    XmlDatabaseHelper.XmlRow ss_rows = db.AddXmlRow("States");
		////    for (int i = 0; i < states.Count; i++)
		////        ((CTMCState)states[i]).id = i;
		////    double sumprob = 0;
		////    foreach (CTMCState obj in states)
		////    {
		////        XmlDatabaseHelper.XmlRow row = ss_rows.AddXmlRow("State");
		////        row.Attributes.Add("index", obj.id.ToString());

		////        if (exportStateValue)
		////        {
		////            XmlDatabaseHelper.XmlRow stateValueRow = row.AddXmlRow("Statevalue");
		////            //foreach (SMLib.Formalism.VaribalesCollection.Variable v in model.Variables)
		////            //{

		////            //    object r = (obj.content).GetType().InvokeMember(v.ID, BindingFlags.GetField, null, obj.content, null);
		////            //    if (r.GetType().IsArray)
		////            //    {

		////            //        string value = r.GetType().ToString() + "{";
		////            //        int i = 0;
		////            //        foreach (object item in (r as Array))
		////            //        {
		////            //            value += (i > 0) ? ("," + item.ToString()) : (item.ToString());
		////            //            i++;
		////            //        }
		////            //        value += "}";
		////            //        stateValueRow[v.ID] = value;
		////            //        //object collection = r as IEnumerable<object>;
		////            //        //stateValueRow[v.ID] = r.ToString();
		////            //        //_Type t = obj.currentState.GetType().GetElementType();
		////            //        //r.GetType().InvokeMember(
		////            //        //int[] array = new int[] { 0, 1, 2 };
		////            //        //object obj = array;
		////            //        //t = o.GetType().GetElementType();
		////            //        //object[] b = (t.GetElementType())o;

		////            //    }
		////            //    else
		////            //    {
		////            //        stateValueRow[v.ID] = r.ToString();
		////            //    }
		////            //}
		////        }

		////        if (exportTransitions)
		////        {
		////            XmlDatabaseHelper.XmlRow trrow = row.AddXmlRow("Transitions");
		////            foreach (CTMCState.Transition t in obj.Transitions)
		////            {
		////                XmlDatabaseHelper.XmlRow r = trrow.AddXmlRow("Destination");
		////                r.Value = ((CTMCState)t.Destination).id.ToString();
		////                r.Attributes.Add("Rate", t.Rate.ToString());
		////                //if (t.actionName != "") r.Attributes.Add("Action", t.actionName);
		////                //if (t.isControllable)
		////                //    r.Attributes.Add("isControllable", "true");
		////                //else
		////                //    r.Attributes.Add("isControllable", "false");
		////            }
		////        }
		////        if (exportProbabilities)
		////        {
		////            sumprob += obj.probability;
		////            row.Attributes.Add("probability", obj.probability.ToString());
		////        }
		////        if (obj.rewardsvalue != null)
		////        {
		////            XmlDatabaseHelper.XmlRow rewardXMLRow = row.AddXmlRow("Rewards");
		////            for (int j = 0; j < obj.rewardsvalue.Count; j++)
		////            {
		////                rewardXMLRow.AddXmlRow(obj.rewardsvalue.Keys[j])
		////                   .Value = obj.rewardsvalue.Values[j].ToString();
		////            }

		////        }
		////    }
		////    if (exportProbabilities)
		////    {
		////        ss_rows.Attributes.Add("sumprob", sumprob.ToString());
		////    }

		////    XmlDatabaseHelper.XmlRow inits = db.AddXmlRow("Initials");
		////    //foreach (InitialState state in initialstate)
		////    //{
		////    //    XmlDatabaseHelper.XmlRow init = inits.AddXmlRow("State");
		////    //    init["index"] = state.state.i.ToString();
		////    //    init["P"] = state.probabilty.ToString();
		////    //}

		////    if (Rewards.Count > 0)
		////    {
		////        inits = db.AddXmlRow("Rewards");
		////        //foreach (Formalism.RewardsCollection.SDESReward r in ((SDESModel)model).Rewards)
		////        //{

		////        //    XmlDatabaseHelper.XmlRow init = inits.AddXmlRow("reward");
		////        //    init["ID"] = r.ID;
		////        //    init["Value"] = Rewards[r.ID].ToString();
		////        //}
		////    }
		////    db.WriteXml(path, "TranSys");
		////}



		//#endregion

		/////<summary>
		/////Load the currentState space from a specified file 
		/////</summary>
		///// <param name="path">Used to indicate the path.</param>
		//public static CTMC_StateSpace LoadFromXML(string path)
		//{
		//    XmlDatabaseHelper db = XmlDatabaseHelper.ReadXml(path);
		//    XmlDatabaseHelper.XmlRow[] statesRow = db["States"][0].RowsOf("State");
		//    CTMC_StateSpace ss = new CTMC_StateSpace();
		//    for (int i = 0; i < statesRow.Length; i++)
		//    {
		//        CTMCState s = new CTMCState(i, null);
		//        //s.i = i;
		//        ss.states.Add(s);
		//    }

		//    try
		//    {
		//        int srcID = 0, dstID = 0;

		//        foreach (XmlDatabaseHelper.XmlRow stateRow in db["States"][0].RowsOf("State"))
		//        {
		//            srcID = int.Parse(stateRow.GetAttribute("index"));
		//            srcID--;
		//            CTMCState srcState = (CTMCState)ss.states[srcID];
		//            //if (stateRow.GetAttribute("isFinalState").Equals("true"))
		//            //    srcState.finalState = true;
		//            //else
		//            //    srcState.finalState = false;
		//            Int32.TryParse(stateRow.GetAttribute("index"), out srcState.id);

		//            foreach (XmlDatabaseHelper.XmlRow destinationRow in stateRow["Transitions"].RowsOf("Destination"))
		//            {
		//                dstID = int.Parse(destinationRow.Value);
		//                dstID--;
		//                bool isControllable;
		//                Boolean.TryParse(destinationRow.GetAttribute("isControllable"), out isControllable);
		//                srcState.Transitions.Add(new CTMCState.Transition(0, (CTMCState)ss.states[dstID]));
		//            }
		//        }

		//    }
		//    catch //(Exception e)
		//    {
		//        //System.Windows.Forms.MessageBox.Show("Error in reading currentState space!");
		//        ss = null;
		//    }
		//    return ss;
		//}

		public override CTMCState DestinationOf (CTMCState.Transition t)
		{
			return t.Destination;
		}
	}


}
